Process Analysis Toolkit (PAT) 3.5 Help |
PCSP System is based on CSP Module extended
with probability syntax as highlighted below. Other syntax can be found in CSP Grammar
Rules. assertion
: '#' 'assert'
definitionRef
(
( '|=' ( '(' | ')' | '[]' | '<>' | ID | STRING | '!' | '?' |
'&&' | '||' | '->' | '<->' | '/\\' | '\\/' | '.' | INT )+
withClause
| 'deadlockfree'
withClause
| 'nonterminating'
withClause
|
'deterministic'
| 'reaches' ID
withClauseReach
| 'refines' definitionRef
withClauseReach
| 'refines' '<F>' definitionRef
| 'refines' '<FD>' definitionRef
)
';'
; withClause ; withClauseReach ; pcaseCondition floatNumber
;
: 'with' ('pmax' | 'pmin' | 'prob')
: 'with' ('pmax' | 'pmin' | 'prob' | 'min' '(' expression ')' | 'max' '('
expression ')')
caseExpr
:
'case'
'{' caseCondition+
('default'
':'
elsec=interleaveExpr)?
'}'
|
'pcase'
'{'
pcaseCondition+
('default' ':'
elsec=interleaveExpr)?
'}'
|
ifExpr
;
:'['
floatNumber ']' ':'
interleaveExpr
;
: INT ('.' INT)?